
* Types, Values, and Effects

** Evaluation and Execution 

*** Imperative model of computation

Programs are a sequence of COMMANDS

A command 1) Examines the contents of memory
          2) Performs a simple computation 
          3) Modifies the memory
          4) Continues with the next instruction
  
Commands are executed for their EFFECT on the memory (IO, Network)

*** ML model of computation

Computation by EVALUATION OF EXPRESSIONS rather than EXECUTION OF
COMMANDS

f(x) = 2 x^2 + x + 1

Close relationship to math = easier mathematical techniques for
reasoning

Why is it hard to reason about imperative programs?

Commands as a special case

** ML computation model

Expressions

1) May or may not have a TYPE
2) May or may not have a VALUE
3) May or may not cause an EFFECT

Type is a description of the value an expresion yields (if it yields
one at all)

Ex:  If e : int, value is a number
        e : float, value is a floating point number

Type is a PREDICTION of the form of the value

Every expression has at least one type.  
 - Those that do are WELL-TYPED
 - Those that do not are ILL-TYPED.  Ineligible for evaluation.
 - TYPE-CHECKER tells which expressions are well or ill typed

A well-typed expression is evaluated to determine its value if it has one

  It may not have a value if
   - nontermination
   - exception 

  If it has a value
  - type bool => true or false, cannot be 7, 3.14

An expression may also cause an effect

 - Exception
 - Modifying memory
 - IO

Type says nothing about effects!!

For us, no effects for awhile
 
*** Type Checking

**** What is a type?

1) A NAME for the type
2) The VALUES of the type
3) The OPERATIONS on the values of the type 

**** Example

INT

Name: int
Values: 0, 1, -1, 2
Operations: + - * / div mod

1 + 3 mod 5

Formation of expressions is governed by TYPING RULES

-----------
 1 : int

 n : int    m : int
--------------------
 n + m : int


          -------   -------
          3 : int   5 : int
-------   -----------------
1 : int   3 mod 5 : int
-----------------------
1 + 3 mod 5 : int
 
*** Evaluation

5 --> 5
2 + 3 --> 5 

n --> N  m --> M   N + M = k   
-----------------------------
n + m --> k

** Types, Types, Types

*** Float

 - Values: 3.14
 - Operations: +.

*** Char

 - Values: 'c'
 - Ops: code, <

*** String

 - Values: "Sean"
 - Ops: ^ length 

*** Bool
  
 - Values: true, false
 - Ops: && , if .. then .. else


e1 : bool  e2 : tau  e3 : tau
----------------------------
if e1 then e2 else e3 : tau


 e1 --> true   e2 --> e
--------------------------
if e1 then e2 else e3 --> e

 e1 --> false   e3 --> e
--------------------------
if e1 then e2 else e3 --> e


** Type Errors

Now we have more than one type, enough rope to hang ourselves!

2 + "sean"

if true then 5 else 4 + "sean"

* Declarations

** Variables

Values can be assigned to variables. 

Vars can then be used in expressions to stand for their value.  

Variables in ML DO NOT VARY!

** Basic bindings

*** Type bindings

Also type binding

  type real = float
  type count = int and average = real

*** Value bindings

let m = 3 + 2
let m : int = 3 + 2

let pi : float = 3.14
and e : real = 2.17

let x : float = sin pi

SUBSTITUTION PRINCIPLE

To evaluate "cos x", replace x by its value, then compute as before

** Compund declarations

val m : int = 3 + 2
val n : int = m * m 

Binding is not assignment!  But you can SHADOW a binding

val n : float = 3.4 

Different type, different value

** Limiting scope

let x = 5 in
  x + x

let m : int = 2
let r : int =
  (let m : int = 3 in
   let n : int = m * m in
    m * n) * m 

** Typing and evaluation 

1) Type checking must take account of the declared type of a variable
2) Evaluation must take account of the declared value of a variable

*** Environments
 
Used for type checking and evaluation
 - Type environment
 - Value environment    
 
Declarations:

  val m : int = 0
  val x : real = Math.sqrt(2.0)
  val c : char = #"a"

Type env:

  val m : int
  val x : real
  val c : char

Value env:

  val m = 0
  val x = 1.414
  val c = #"a"

Extend typing rules

typeenv |- exp : typ

valenv |- exp --> val

* Functions

** Functions as Templates

ABSTRACT the data from a calculation, leaving behind the
bare PATTERN.  The pattern is INSTANTIATED with data.

*** Example
2 * (3 + 4)

Data = 2,3,4

O * (O + O)

Data = 2,3

O * (O + 4)

Data = + *

2 O 3 O 4

A complete expression can be recovered by filling in holes with data.

Names for the holes = variables
Instantiation = substitution
Pattern = function of the variables

*** Analogy

x^2 + 2x + 1

x is a fixed but unknown quantity

f(x) = x^2 + 2 x + 1

x^2 + 2 x y + y^2

What are the variables? x, y, x and y?

f(x) = ...
f(y) = ...
f(x,y) = ...    

Separate the NAME of the function from the function itself.

f : R -> R : x |-> ...

let f x = x^2 + 2 x + 1
let f x y = x^2 + 2 x y + y^2
...
let f : real -> real = fun x y -> ...

let fact : int -> int =
  fun n -> if n 
